Nuprl Lemma : es-snds-index_wf
0,22
postcript
pdf
the_es
:ES,
l
:IdLnk,
e
:E,
n
:
. snds(
l
, before(
e
,
n
))
(Msg on
l
) List
latex
Definitions
E
,
IdLnk
,
ES
,
snds(
l
, before(
e
,
n
))
,
as
@
bs
,
snds(
l
;before(
e
))
,
firstn(
n
;
as
)
,
(Msg on
l
)
,
sends(
l
;
e
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
es-sends
wf
,
firstn
wf
,
es-snds
wf
,
es-Msgl
wf
,
append
wf
,
event
system
wf
,
IdLnk
wf
,
es-E
wf
origin
the_es:ES, l:IdLnk, e:E, n:
. snds(l, before(e,n)) 
(Msg on l) List the_es:ES, l:IdLnk, e:E, n:. snds(l, before(e,n)) (Msg on l) List x:A. B(x) T